(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun T1_18564 () (_ BitVec 8))
(declare-fun T1_18521 () (_ BitVec 8))
(declare-fun T1_18478 () (_ BitVec 8))
(declare-fun T1_18428 () (_ BitVec 8))
(declare-fun T1_18379 () (_ BitVec 8))
(declare-fun T2_18377 () (_ BitVec 16))
(declare-fun T1_18375 () (_ BitVec 8))
(declare-fun T2_17983 () (_ BitVec 16))
(declare-fun T1_17974 () (_ BitVec 8))
(declare-fun T4_17975 () (_ BitVec 32))
(declare-fun T1_18377 () (_ BitVec 8))
(declare-fun T1_18378 () (_ BitVec 8))
(declare-fun T1_17983 () (_ BitVec 8))
(declare-fun T1_17984 () (_ BitVec 8))
(declare-fun T1_17975 () (_ BitVec 8))
(declare-fun T1_17976 () (_ BitVec 8))
(declare-fun T1_17977 () (_ BitVec 8))
(declare-fun T1_17978 () (_ BitVec 8))
(assert (let ((?v_22 ((_ zero_extend 24) T1_18564)) (?v_18 ((_ zero_extend 24) T1_18521)) (?v_14 ((_ zero_extend 24) T1_18478)) (?v_10 ((_ zero_extend 24) T1_18428)) (?v_6 ((_ zero_extend 24) T1_18379)) (?v_21 ((_ zero_extend 16) T2_18377)) (?v_0 ((_ zero_extend 24) (_ bv1 8))) (?v_7 ((_ zero_extend 24) T1_18375)) (?v_3 ((_ zero_extend 16) T2_17983)) (?v_2 (bvsub ((_ zero_extend 24) T1_17974) (_ bv8 32)))) (let ((?v_4 (bvadd (bvadd (bvadd (bvadd ?v_2 (_ bv1598438 32)) ?v_3) (_ bv7 32)) ?v_7))) (let ((?v_8 (bvadd (bvadd ?v_4 (_ bv3 32)) ?v_6))) (let ((?v_12 (bvadd (bvadd ?v_8 ?v_0) ?v_10))) (let ((?v_16 (bvadd (bvadd ?v_12 ?v_0) ?v_14))) (let ((?v_17 (bvsub ?v_16 (_ bv1598407 32)))) (let ((?v_19 (bvsub (bvadd (bvadd ?v_17 (_ bv1598408 32)) ?v_18) (_ bv1 32))) (?v_20 (bvadd ?v_17 (_ bv1598450 32))) (?v_13 (bvsub ?v_12 (_ bv1598407 32)))) (let ((?v_15 (bvsub (bvadd (bvadd ?v_13 (_ bv1598408 32)) ?v_14) (_ bv1 32))) (?v_9 (bvsub ?v_8 (_ bv1598407 32)))) (let ((?v_11 (bvsub (bvadd (bvadd ?v_9 (_ bv1598408 32)) ?v_10) (_ bv1 32))) (?v_5 (bvsub ?v_4 (_ bv1598405 32))) (?v_1 (bvsub (bvadd (bvadd ?v_16 ?v_0) ?v_18) (_ bv1598407 32)))) (and true (= T4_17975 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_17978) (_ bv8 32)) ((_ zero_extend 24) T1_17977)) (_ bv8 32)) ((_ zero_extend 24) T1_17976)) (_ bv8 32)) ((_ zero_extend 24) T1_17975))) (= T2_17983 (bvor (bvshl ((_ zero_extend 8) T1_17984) (_ bv8 16)) ((_ zero_extend 8) T1_17983))) (= T2_18377 (bvor (bvshl ((_ zero_extend 8) T1_18378) (_ bv8 16)) ((_ zero_extend 8) T1_18377))) (bvule (bvsub (bvadd (bvadd ?v_1 (_ bv1598408 32)) ?v_22) (_ bv1 32)) (bvadd ?v_1 (_ bv1598448 32))) (not (= (bvadd (bvadd ?v_2 (_ bv30 32)) (_ bv1598408 32)) (_ bv0 32))) (bvult (_ bv0 32) ?v_3) (not (= ?v_3 (_ bv0 32))) (= T4_17975 ?v_3) (bvult (bvadd ?v_5 (_ bv1598446 32)) (bvsub (bvadd (bvadd ?v_5 (_ bv1598408 32)) ?v_6) (_ bv1 32))) (bvult ?v_7 (_ bv8 32)) (not (= ?v_7 (_ bv0 32))) (= ?v_7 (_ bv1 32)) (bvult (bvadd ?v_9 (_ bv1598428 32)) ?v_11) (bvult (bvadd ?v_9 (_ bv1598412 32)) ?v_11) (not (= ?v_21 (_ bv0 32))) (bvult (bvadd ?v_13 (_ bv1598442 32)) ?v_15) (bvult (bvadd ?v_13 (_ bv1598418 32)) ?v_15) (not (= ?v_20 ?v_19)) (bvule ?v_19 ?v_20) (= (bvadd (bvadd (bvadd (bvadd (bvadd ?v_21 (bvsub (_ bv4294967295 32) ?v_6)) (bvsub (_ bv4294967295 32) ?v_10)) (bvsub (_ bv4294967295 32) ?v_14)) (bvsub (_ bv4294967295 32) ?v_18)) (bvsub (_ bv4294967295 32) ?v_22)) (_ bv0 32)))))))))))))
(check-sat)
(exit)
